COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00005 ENDMK
C⊗;


(DEFPROP INSTFNS
 (NIL INST ISVAR SUBLIS COMMINST ASSOCINST)
VALUE)

(DEFPROP INST
 (LAMBDA(E M P)
  (COND	((EQ P (QUOTE NO)) P)
	((ATOM M)
	 (COND ((ISVAR M)
		((LAMBDA (W) (COND ((NULL W) (CONS (CONS M E) P)) ((EQUAL (CDR W) E) P) (T (QUOTE NO))))
		 (ASSOC M P)))
	       ((EQ M E) P)
	       (T (QUOTE NO))))
	((ATOM E) (QUOTE NO))
	((COMMUTATIVE (CAR M)) (COND ((ATOM E) @NO)
		(T (COMMINST (CDR E) (CDR M) (INST (CAR E) (CAR M) P) NIL))))
	(T (INST (CDR E) (CDR M) (INST (CAR E) (CAR M) P)))))
EXPR)

(DE COMMINST (LEXP LPAT A U)
	(COND ((EQ A @NO) @NO)
	((ATOM LPAT)
		(COND ((ISVAR LPAT)
			((LAMBDA (W) (COND ((NULL W) (CONS (CONS LPAT (APPEND
LEXP U)) A)) ((AND (EQUAL (CDR W) LEXP) (NULL U)) A) (T @NO))) (ASSOC LPAT A)))
((EQ LPAT LEXP) A) (T @NO)))
			((NULL LEXP) @NO)
			(T ((LAMBDA (W) (COND ((EQ W @NO)
(COMMINST (CDR LEXP) LPAT A (CONS (CAR LEXP) U)))
						(T 
(COMMINST (APPEND U (CDR LEXP)) (CDR LPAT) W NIL)))) (INST (CAR LEXP)
(CAR LPAT) A)))))


(DEFPROP ISVAR
 (LAMBDA (M) (MEMBER M (QUOTE (U V W X Y Z))))
EXPR)

(DEFPROP SUBLIS
 (LAMBDA(E P)
  (COND	((ATOM E) ((LAMBDA (W) (COND ((NULL W) E) (T (CDR W)))) (ASSOC E P)))
	(T
	 ((LAMBDA (X Y) (COND ((AND (EQ X (CAR E)) (EQ Y (CDR E))) E) (T (CONS X Y))))
	  (SUBLIS (CAR E) P)
	  (SUBLIS (CDR E) P)))))
EXPR)